1. $T$ : Type
\\[0ex]2. $T$ List
\\[0ex]3. $u$ : $T$
\\[0ex]4. $v$ : $T$ List
\\[0ex]5. $\forall$$n$:\{0$\ldots\,\parallel$$v$$\parallel$\}, $i$:\{0..($\parallel$$v$$\parallel$ {-} $n$)$^{-}$\}. nth\_tl($n$;$v$)[$i$] = $v$[($i$+$n$)]
\\[0ex]6. $n$ : \{0$\ldots\,\parallel$$v$$\parallel$+1\}
\\[0ex]7. $i$ : \{0..(($\parallel$$v$$\parallel$+1) {-} $n$)$^{-}$\}
\\[0ex]8. 0 $<$ $n$
\\[0ex]$\vdash$  $v$[($i$+($n$ {-} 1))] = [$u$ / $v$][($i$+$n$)]